j:, f:({0..j}). (n:{0..j}. 0  f(n))  0  0  n < j. f(n) 

latex

Definitions	P  Q, True, T, P  Q, P & Q, i  j < k, x. t(x), {i..j}, , t  T, x(s), P  Q, x:A. B(x), , S  T
Lemmas	qmul zero qrng, qsum wf, int-rational, qsum-const, true wf, squash wf, le wf, qsum-qle, nat wf, rationals wf, int inc rationals, qle wf, int seg wf